Left Termination proof of /tmp/tmpu5koPe/ackermann-ioi.pl

Left Termination of the query pattern ackermann_in_3(g, a, g) w.r.t. the given Prolog program could not be shown:

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

Clauses:

ackermann(0, N, s(N)).
ackermann(s(M), 0, Val) :- ackermann(M, s(0), Val).
ackermann(s(M), s(N), Val) :- ','(ackermann(s(M), N, Val1), ackermann(M, Val1, Val)).

Queries:

ackermann(g,a,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann_in: (b,f,b) (b,b,b) (b,b,f) (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s(x1)
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag
U1_gag(x1, x2, x3) = U1_gag(x3)
ackermann_in_ggg(x1, x2, x3) = ackermann_in_ggg(x1, x2, x3)
ackermann_out_ggg(x1, x2, x3) = ackermann_out_ggg
U1_ggg(x1, x2, x3) = U1_ggg(x3)
U2_ggg(x1, x2, x3, x4) = U2_ggg(x1, x3, x4)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x3)
U1_gga(x1, x2, x3) = U1_gga(x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U3_ggg(x1, x2, x3, x4) = U3_ggg(x4)
U2_gag(x1, x2, x3, x4) = U2_gag(x1, x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa
U1_gaa(x1, x2, x3) = U1_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x4)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x4)
U2_GGG(x1, x2, x3, x4) = U2_GGG(x1, x3, x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U1_GGA(x1, x2, x3) = U1_GGA(x3)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
U1_GGG(x1, x2, x3) = U1_GGG(x3)
U1_GAG(x1, x2, x3) = U1_GAG(x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)
U3_GGG(x1, x2, x3, x4) = U3_GGG(x4)
ACKERMANN_IN_GGG(x1, x2, x3) = ACKERMANN_IN_GGG(x1, x2, x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x4)
ACKERMANN_IN_GGA(x1, x2, x3) = ACKERMANN_IN_GGA(x1, x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, ackermann_in_gga(s(M), N))
U2_GGA(M, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGA(M, Val1)
ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0)
U2_gga(x0, x1)
U3_gga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1
U2_GGA(M, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGA(M, Val1)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x3)
U1_gga(x1, x2, x3) = U1_gga(x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa
U1_gaa(x1, x2, x3) = U1_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))
U2_GAA(M, ackermann_out_gaa) → ACKERMANN_IN_GAA(M)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U2_GAA(M, ackermann_out_gaa) → ACKERMANN_IN_GAA(M)

The remaining pairs can at least be oriented weakly.

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ACKERMANN_IN_GAA(x₁)) = x₁
POL(U1_gaa(x₁)) = 1 + x₁
POL(U1_gga(x₁)) = 0
POL(U2_GAA(x₁, x₂)) = 1 + x₁
POL(U2_gaa(x₁, x₂)) = 1
POL(U2_gga(x₁, x₂)) = 0
POL(U3_gaa(x₁)) = 1
POL(U3_gga(x₁)) = 0
POL(ackermann_in_gaa(x₁)) = 1
POL(ackermann_in_gga(x₁, x₂)) = 0
POL(ackermann_out_gaa) = 1
POL(ackermann_out_gga(x₁)) = 1
POL(s(x₁)) = 1 + x₁

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

R is empty.
The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:none

s = ACKERMANN_IN_GAA(s(M)) evaluates to t =ACKERMANN_IN_GAA(s(M))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ACKERMANN_IN_GAA(s(M)) to ACKERMANN_IN_GAA(s(M)).

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, Val, ackermann_in_gga(s(M), N))
U2_GGG(M, Val, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0)
U2_gga(x0, x1)
U3_gga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, Val, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1, 3 >= 2
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
The graph contains the following edges 1 > 1, 3 >= 3
U2_GGG(M, Val, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
The graph contains the following edges 1 >= 1, 3 > 2, 2 >= 3

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x3)
U1_gga(x1, x2, x3) = U1_gga(x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa
U1_gaa(x1, x2, x3) = U1_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_GAG(M, Val, ackermann_out_gaa) → ACKERMANN_IN_GAG(M, Val)
ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U2_GAG(M, Val, ackermann_out_gaa) → ACKERMANN_IN_GAG(M, Val)
The graph contains the following edges 1 >= 1, 2 >= 2
ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))
The graph contains the following edges 1 > 1, 2 >= 2

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann_in: (b,f,b) (b,b,b) (b,b,f) (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s(x1)
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag(x1, x3)
U1_gag(x1, x2, x3) = U1_gag(x1, x2, x3)
ackermann_in_ggg(x1, x2, x3) = ackermann_in_ggg(x1, x2, x3)
ackermann_out_ggg(x1, x2, x3) = ackermann_out_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3) = U1_ggg(x1, x2, x3)
U2_ggg(x1, x2, x3, x4) = U2_ggg(x1, x2, x3, x4)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
U3_ggg(x1, x2, x3, x4) = U3_ggg(x1, x2, x3, x4)
U2_gag(x1, x2, x3, x4) = U2_gag(x1, x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1)
U1_gaa(x1, x2, x3) = U1_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x1, x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x1, x3, x4)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x1, x3, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x1, x4)
U2_GGG(x1, x2, x3, x4) = U2_GGG(x1, x2, x3, x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U1_GGA(x1, x2, x3) = U1_GGA(x1, x3)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x1, x3)
U1_GGG(x1, x2, x3) = U1_GGG(x1, x2, x3)
U1_GAG(x1, x2, x3) = U1_GAG(x1, x2, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)
U3_GGG(x1, x2, x3, x4) = U3_GGG(x1, x2, x3, x4)
ACKERMANN_IN_GGG(x1, x2, x3) = ACKERMANN_IN_GGG(x1, x2, x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
ACKERMANN_IN_GGA(x1, x2, x3) = ACKERMANN_IN_GGA(x1, x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s(x1)
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag(x1, x3)
U1_gag(x1, x2, x3) = U1_gag(x1, x2, x3)
ackermann_in_ggg(x1, x2, x3) = ackermann_in_ggg(x1, x2, x3)
ackermann_out_ggg(x1, x2, x3) = ackermann_out_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3) = U1_ggg(x1, x2, x3)
U2_ggg(x1, x2, x3, x4) = U2_ggg(x1, x2, x3, x4)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
U3_ggg(x1, x2, x3, x4) = U3_ggg(x1, x2, x3, x4)
U2_gag(x1, x2, x3, x4) = U2_gag(x1, x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1)
U1_gaa(x1, x2, x3) = U1_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x1, x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x1, x3, x4)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x1, x3, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x1, x4)
U2_GGG(x1, x2, x3, x4) = U2_GGG(x1, x2, x3, x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U1_GGA(x1, x2, x3) = U1_GGA(x1, x3)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x1, x3)
U1_GGG(x1, x2, x3) = U1_GGG(x1, x2, x3)
U1_GAG(x1, x2, x3) = U1_GAG(x1, x2, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)
U3_GGG(x1, x2, x3, x4) = U3_GGG(x1, x2, x3, x4)
ACKERMANN_IN_GGG(x1, x2, x3) = ACKERMANN_IN_GGG(x1, x2, x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
ACKERMANN_IN_GGA(x1, x2, x3) = ACKERMANN_IN_GGA(x1, x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 12 less nodes.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
ACKERMANN_IN_GGA(x1, x2, x3) = ACKERMANN_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, N, ackermann_in_gga(s(M), N))
U2_GGA(M, N, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1)
ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, N, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1, 2 > 2
U2_GGA(M, N, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2
ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1)
U1_gaa(x1, x2, x3) = U1_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x1, x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
U2_GAA(M, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAA(M)
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U2_GAA(M, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAA(M)

The remaining pairs can at least be oriented weakly.

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ACKERMANN_IN_GAA(x₁)) = x₁
POL(U1_gaa(x₁, x₂)) = 0
POL(U1_gga(x₁, x₂)) = 0
POL(U2_GAA(x₁, x₂)) = 1 + x₁
POL(U2_gaa(x₁, x₂)) = 0
POL(U2_gga(x₁, x₂, x₃)) = 0
POL(U3_gaa(x₁, x₂)) = 0
POL(U3_gga(x₁, x₂, x₃)) = 0
POL(ackermann_in_gaa(x₁)) = 1
POL(ackermann_in_gga(x₁, x₂)) = 0
POL(ackermann_out_gaa(x₁)) = 0
POL(ackermann_out_gga(x₁, x₂, x₃)) = 0
POL(s(x₁)) = 1 + x₁

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

R is empty.
The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ACKERMANN_IN_GAA(s(M)) to ACKERMANN_IN_GAA(s(M)).

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
U2_GGG(x1, x2, x3, x4) = U2_GGG(x1, x2, x3, x4)
ACKERMANN_IN_GGG(x1, x2, x3) = ACKERMANN_IN_GGG(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
The graph contains the following edges 1 > 1, 3 >= 3
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
The graph contains the following edges 1 >= 1, 4 > 1, 4 > 2, 3 >= 3

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1)
U1_gaa(x1, x2, x3) = U1_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x1, x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))
U2_GAG(M, Val, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAG(M, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U2_GAG(M, Val, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAG(M, Val)
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2
ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))
The graph contains the following edges 1 > 1, 2 >= 2